@book{SF,
  author = {Benjamin C. Pierce and Chris Casinghino and Marco Gaboardi and
                  Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu 
                  and Vilhelm Sjoberg and Brent Yorgey},
  title = {Software Foundations},
  year = {2014},
  publisher = {Electronic textbook},
  plclub = {Yes},
  bcp = {Yes},
  keys = {poplmark,books},
  japanese = {http://proofcafe.org/sf}@article{Hoare:1969:ABC:363235.363259,
 author = {Hoare, C. A. R.},
 title = {An Axiomatic Basis for Computer Programming},
 journal = {Commun. ACM},
 issue_date = {Oct. 1969},
 volume = {12},
 number = {10},
 month = oct,
 year = {1969},
 issn = {0001-0782},
 pages = {576--580},
 numpages = {5},
 url = {http://doi.acm.org/10.1145/363235.363259},
 doi = {10.1145/363235.363259},
 acmid = {363259},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {axiomatic method, formal language definition, machine-independent programming, program documentation, programming language design, theory of programming' proofs of programs},
}
}

@ARTICLE{miniAES,
    author = {Raphael Chung-wei Phan},
    title = {Mini Advanced Encryption Standard (Mini-AES): A Testbed for Cryptanalysis},
    journal = {Students, Cryptologia},
    year = {2002},
    pages = {283--306}
}

@book{Stallings,
  title={Cryptography and Network Security: Principles and Practice},
  author={Stallings, W.},
  isbn={9780137056323},
  lccn={2010483725},
  url={http://books.google.ca/books?id=3alWQwAACAAJ},
  year={2011},
  publisher={Prentice Hall}
}

@book{cpdt,
  title={Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant},
  author={Chlipala, A.},
  isbn={9780262026659},
  lccn={2013012837},
  url={http://books.google.com.uy/books?id=8msTAgAAQBAJ},
  year={2013},
  publisher={MIT Press}
}

@article{Standards2001,
  added-at = {2011-02-14T16:52:54.000+0100},
  added-by = {enm},
  author = {of Standards, National Institute and Technology},
  biburl = {http://www.bibsonomy.org/bibtex/2df48e6a03df4a6277d851da16c1d2dc3/fohv},
  date-modified = {2006-08-22 11:34:23 +0200},
  interhash = {97e1e71382e3c5ab420aa56cb4fe4499},
  intrahash = {df48e6a03df4a6277d851da16c1d2dc3},
  journal = {NIST FIPS PUB 197},
  keywords = {imported},
  timestamp = {2011-02-14T16:52:54.000+0100},
  title = {Advanced Encryption Standard},
  year = 2001
}

@misc{des,
  added-at = {2009-01-14T00:43:43.000+0100},
  author = {{National Institute of Standards and Technology}},
  biburl = {http://www.bibsonomy.org/bibtex/267a96ce3e5adcc0327fa1ae64da0ef7d/dret},
  description = {dret'd bibliography},
  howpublished = {FIPS Publication 46-2},
  interhash = {49603029d7de814aa9ce3d10b70b0058},
  intrahash = {67a96ce3e5adcc0327fa1ae64da0ef7d},
  keywords = {imported},
  month = {December},
  timestamp = {2009-01-14T00:43:43.000+0100},
  title = {Data Encryption Standard},
  topic = {des[1] dea[1]},
  year = 1993
}

@Manual{Coq:manual,
  title =        {The Coq proof assistant reference manual},
  author =       {\mbox{The Coq development team}},
  organization = {LogiCal Project},
  note =         {Version 8.4},
  year =         {2012},
  url =          "http://coq.inria.fr"
}

@misc{rijndael,
    author        = {Joan Daemen and Vincent Rijmen},
    howpublished  = {AES submission},
    title         = {AES Proposal: {{\sc Rijndael}}},
    year          = {1999}
}

@misc{CompCert,
  author = {Xavier Leroy and al.},
  title = {CompCert: compilers you can formally  trust},
  year = 2010
}

@misc{Ynot,
  title = {The Ynot project},
  howpublished = {\url{http://ynot.cs.harvard.edu/}},
  note = {(Último acceso Noviembre 2014)}
}

@misc{certicrypt,
  author = {G. Barthe, B. Grégoire, F. Olmedo, and S. Zanella-Béguelin and al},
  title = {CertiCrypt: Computer-Aided Cryptographic Proofs in Coq},
  howpublished = {\url{http://certicrypt.gforge.inria.fr/}},
  note = {(Último acceso Noviembre 2014)},
  annote = 2010
}

@misc{Matrices,
  author = {N. Magaud},
  title = {Ring properties for square matrices},
  howpublished = {\url{http://coq.inria.fr/pylons/pylons/contribs/view/Matrices/trunk}},
  note = {(Último acceso Noviembre 2014)},
  annote = 2010
}

@techreport{cic,
    hal_id = {inria-00076024},
    title = {The calculus of constructions},
    author = {Coquand, T. and Huet, G{\'e}rard},
    institution = {INRIA},
    number = {RR-0530},
    year = {1986},
    month = May
}

@book{turing,
 author = {Brainerd, Walter},
 title = {Theory of computation},
 publisher = {Wiley},
 year = {1974},
 address = {New York},
 isbn = {0471095850}
}

@article{Hoare:1969:ABC:363235.363259,
 author = {Hoare, C. A. R.},
 title = {An Axiomatic Basis for Computer Programming},
 journal = {Commun. ACM},
 volume = {12},
 number = {10},
 year = {1969},
 issn = {0001-0782},
 pages = {576--580},
 numpages = {5}
}

@misc{nist_validation,
  author = "National Institute of Standards and Technology",
  title = "Advanced Encryption Standard Algorithm Validation List",
  year = {Oct. 2014}
}

@book{rijndael_libro,
  author    = {Joan Daemen and
               Vincent Rijmen},
  title     = {The Design of Rijndael: AES - The Advanced Encryption Standard},
  publisher = {Springer},
  series    = {Information Security and Cryptography},
  year      = {2002},
  isbn      = {3-540-42580-2, 978-3-642-07646-6},
  ee        = {http://dx.doi.org/10.1007/978-3-662-04722-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{campos_finitos,
 author = {Lidl, Rudolf and Niederreiter, Harald},
 title = {Introduction to Finite Fields and Their Applications},
 year = {1986},
 isbn = {0-521-30706-6},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

@book{cryptography,
 author = {Menezes, Alfred J. and Vanstone, Scott A. and Oorschot, Paul C. Van},
 title = {Handbook of Applied Cryptography},
 year = {1996},
 isbn = {0849385237},
 edition = {1st},
 publisher = {CRC Press, Inc.},
 address = {Boca Raton, FL, USA},
}

@MISC{cache,
    author = {Eran Tromer and Dag Arne Osvik and Adi Shamir},
    title = {Efficient Cache Attacks on AES, and Countermeasures},
    year = {2009}
}

@MISC{virtualcert,
    author = {G. Betarte, C. Luna y J.D. Campo},
    title = {Virtual Cert, descripción del modelo},
    year = {2010}
}

@misc{PolarSSL,
  title = {PolarSSL},
  howpublished = {\url{https://polarssl.org/}},
  note = {(Último acceso Noviembre 2014)}
} 

@misc{Libgcrypt,
  title = {Libgcrypt},
  howpublished = {\url{http://www.gnu.org/software/libgcrypt/}},
  note = {(Último acceso Noviembre 2014)}
}

@misc{OpenSSL,
  title = {OpenSSL},
  howpublished = {\url{https://www.openssl.org/}},
  note = {(Último acceso Noviembre 2014)}
}

@misc{Crypto++,
  title = {Crypto++},
  howpublished = {\url{http://www.cryptopp.com/}},
  note = {(Último acceso Noviembre 2014)}
}

@misc{Botan,
  title = {Botan},
  howpublished = {\url{http://botan.randombit.net/}},
  note = {(Último acceso Noviembre 2014)}
}

@misc{Oracle_Crypto,
  title = {Oracle Crypto Spec},
  howpublished = {\url{http://docs.oracle.com/javase/8/docs/technotes/guides/security/crypto/CryptoSpec.html}},
  note = {(Último acceso Noviembre 2014)}
}

@misc{Bouncy_Castle,
  title = {Bouncy Castle},
  howpublished = {\url{http://bouncycastle.org/java.html}},
  note = {(Último acceso Noviembre 2014)}
}

@ARTICLE{rsa,
    author = {R.L. Rivest and A. Shamir and L. Adleman},
    title = {A Method for Obtaining Digital Signatures and Public-Key Cryptosystems},
    journal = {Communications of the ACM},
    year = {1978},
    volume = {21},
    pages = {120--126}
}

@MISC{Codigo,
  title = {Código fuente {C}oq desarrollado en este trabajo.},
  howpublished ={\url{http://www.fing.edu.uy/inco/grupos/gsi/index.php?page=proygrado&locale=es}}
}
